4. 类型系统
项，也称为表达式，是 Lean 核心语言中最基本的语义单元。 它们由用户编写的语法经过繁释器生成。 Lean 的类型系统将各项和它们的类型(type)关联起来，而类型本身也是项。 类型可以被看作是表示一个集合，而项表示该集合中的具体元素。 如果某个项根据 Lean 的类型论规则有一个类型，则称它是良型的（well-typed）。 只有良型的项才有意义。
项是一种依值类型 λ-演算：它们包含函数抽象、应用、变量以及 let-绑定。
除了绑定变量外，项语言中的变量还可以引用构造子、类型构造子、递归子、已定义常量或者不透明常量（opaque constant）。
数据构造子、类型构造子、递归子和不透明常量不会被代换，而已定义常量可以被其定义替换。
一个演绎（derivation）通过明确地指明具体应用了哪些推断规则，来展示某项的良型性。 在实际使用中，良型的项本身就代表了证明其良型性的推理过程。 Lean 的类型论可以由良型的项完全可以重建出对应的演绎过程，这大大减少了存储完整演绎所需的开销，而同时仍然能够表达现代数学中的推理。 这意味着证明项已足以作为定理成立的证据，并且可以被独立的系统验证。
除了拥有类型，项之间还存在定义等价关系。 定义等价是可机械化检验的关系，用于在语法上将项根据其计算行为视作等价。 定义等价包含如下几种规约形式：
- β-规约（beta）
将函数抽象应用到实参时，通过对绑定变量做代换来实现
- δ-规约（delta）
将已定义常量出现的地方用其定义值替换
- ι-规约（iota）
归约以构造子为目标的递归器（即原始递归）
- ζ-规约（zeta）
用定义值替换被
let绑定的变量- 商类型规约(Quotient reduction)
应用于商的元素时规约商类型函数的提升算子(lifting operator)
若项中所有可能的规约都已执行完毕，则该项处于 规范形式。
定义等价包括函数和单构造子归纳类型的 η-等价。
也就是说，fun x => f x 与 f 是定义等价的；而若 S 是一个带有字段 f1 和 f2 的结构体，那么 S.mk x.f1 x.f2 与 x 定义等价。
同时还具备 证明无关性：同一命题的任意两个证明项是定义等价的。
定义等价关系具有自反性、对称性，但并不具有传递性。
定义等价被用于转换(conversion)：如果项a和项b是定义等价的，那么如果项c有a或b的类型，那么c也拥有另一个类型。
由于定义等价包括规约，因此类型可以通过数据计算得出。
计算类型
当传入一个自然数时，LengthList 这个函数会得出一个类型，该类型对应于长度恰好等于这个数的列表：
def LengthList (α : Type u) : Nat → Type u
| 0 => PUnit
| n + 1 => α × LengthList α n
由于 Lean 的元组按右结合嵌套，因此无需多层括号：
example : LengthList Int 0 := ()
example : LengthList String 2 :=
("Hello", "there", ())
如果长度与元素项数不匹配，则计算出的类型与项类型不符合：
example : LengthList String 5 :=
("Wrong", "number", ())
Application type mismatch: In the application
("number", ())
the argument
()
has type
Unit : Type
but is expected to have type
LengthList String 3 : Type
Lean 的基本类型包括 宇宙、函数类型、商类型构造器 Quot，以及 归纳类型的 类型构造子。
已定义常量、递归子的应用、函数应用、公理 或 不透明常量(opaque constant) 也都可以作为类型出现，就像它们能出现在普通项的位置一样。
